###                                     ###
### README: PROOFS FOR 'BEYOND THE PSR' ###
###                                     ###

This folder contains the formal proofs verifying the arguments presented in the paper: "Beyond the PSR: A Necessary Entity from a Transmundane Condition of Possibility", archived at https://doi.org/10.5281/zenodo.19629115

***

### DEFINITIONS ###

**Axiomatic system:** A two-sorted FOL mimicking QKB with additional axioms called alpha, beta, gamma and delta.

**Conclusion:** The existence of a necessary entity.

**WL-PSR*:** That every actual contingent entity has an actual or non-actual reason.

**S-PSR:** That every actual entity has an actual reason.

**L-PSR:** That every actual contingent entity has an actual reason.

**W-PSR:** That every actual entity has an actual or non-actual reason.

**(F):** The relation between two entities a and b such that, if a exists in a world w not in a world v, then b exists in v.

**(1):** That every entity is contingent.

***

### FILES OVERVIEW ###

1) **Name:** argument_prover9.txt
   **Tool:** Prover9 Automated Theorem Prover (via pyprover9, in Google Colab)
   **Description:** Generates a derivation of the conclusion within the axiomatic system.

2) **Name:** weaker_S-PSR.txt
   **Tool:** Prover9 Automated Theorem Prover (via pyprover9, in Google Colab)
   **Description:** Generates a derivation of WL-PSR* from S-PSR.

3) **Name:** weaker_L-PSR.txt
   **Tool:** Prover9 Automated Theorem Prover (via pyprover9, in Google Colab)
   **Description:** Generates a derivation of WL-PSR* from L-PSR.

4) **Name:** weaker_W-PSR.txt
   **Tool:** Prover9 Automated Theorem Prover (via pyprover9, in Google Colab)
   **Description:** Generates a derivation of WL-PSR* from W-PSR.

5) **Name:** entailment_F.txt
   **Tool:** Prover9 Automated Theorem Prover (via pyprover9, in Google Colab)
   **Description:** Generates a derivation of (F) from alpha and (1).

6) **Name:** argument_lean.txt
   **Tool:** Lean Theorem Prover (in lean-lang)
   **Description:** Step-by-step derivation of the conclusion within the axiomatic system.

7) **Name:** axiom_coherence.in
   **Tool:** Mace4 Model Searcher
   **Description:** Searches for a model that would satisfy all the axioms. If it finds one: the axiomatic system is coherent.

8) **Name:** independence_alpha.in
   **Tool:** Mace4 Model Searcher
   **Description:** Searches for a model that would satisfy all the axioms except alpha. If it finds one: the axiom alpha is independent.

9) **Name:** independence_beta.in
   **Tool:** Mace4 Model Searcher
   **Description:** Searches for a model that would satisfy all the axioms except beta. If it finds one: the axiom beta is independent.

10) **Name:** independence_gamma.in
   **Tool:** Mace4 Model Searcher
   **Description:** Searches for a model that would satisfy all the axioms except gamma. If it finds one: the axiom gamma is independent.

11) **Name:** independence_delta.in
   **Tool:** Mace4 Model Searcher
   **Description:** Searches for a model that would satisfy all the axioms except delta. If it finds one: the axiom delta is independent.

12) **Name:** independence_PSR.in
   **Tool:** Mace4 Model Searcher
   **Description:** Searches for a model that would satisfy the negation of WL-PSR* within the axiomatic system. If it finds one: the 
                    axiomatic system does not entail the WL-PSR* or stronger versions of the PSR.

***

***                       ***
*** HOW TO RUN THE PROOFS ***
***                       ***

Each tool verifies the results according to its native semantics: Prover9 produces derivations in first-order logic, Lean checks proofs via type-theoretic verification, and Mace4 searches for finite models. 

### PROOF IN PROVER9 ###

  1. Go to: https://colab.research.google.com/
  2. Click on: File -> New notebook
  3. Copy-paste the source code found in argument_prover9.txt
  4. Click on: execute cell (the "play symbol")
  5. If the result is '*PROVED*' followed by an explicit proof, the theorem is proved.

N.B.: The code has been optimized for the "pyprover9" wrapper, which is available in Google Colab environments. The files can also be executed locally with a standard Prover9 installation; however, the Colab-based workflow is the most accessible option.


### PROOF IN LEAN ###

  1. Go to: https://live.lean-lang.org/
  2. Copy-paste the source code found in argument_lean.txt
  3. If no errors appear in 'messages' and there are no 'sorry's in the code, the derivation is correct.

N.B.: live.lean-lang environment provides a standard Lean 4 toolchain in a browser-based interface. The same files can be executed locally using a standard Lean 4 installation.


### PROOFS IN MACE4 ###

  1. On OS Windows, a Linux environment such as WSL should be used. See: https://learn.microsoft.com/windows/wsl/
  2. In the Linux shell, write the following commands:
 
        2.1. sudo apt update
        2.2. sudo apt install build-essential
        2.3. sudo apt install wget
        2.4. wget https://www.cs.unm.edu/~mccune/ladr/ladr-2009-11A.tar.gz
        2.5. tar xzf ladr-2009-11A.tar.gz
        2.6. cd ladr-2009-11A
        2.7. make all
        
  3. Copy all the '.in' proof files in the directory where mace4 is found (generally, it's LADR-2009-11A/bin)
  4. In the Linux shell, write the following commands:
  
        4.1. cd ~/LADR-2009-11A/bin           (assuming that 'bin' is the directory where mace4 is found)
        4.2. ./mace4 -f independence_alpha.in (or the name of another file)

  5. All the files should give 'model found', proving axiom independence.

N.B.: This procedure installs Mace4 via the LADR distribution. Unlike Prover9 and Lean, Mace4 is typically used via a local installation. It can also be run in macOS or ChromeOS (e.g., via Crostini) environments supporting Linux.

  
***

### CONCEPT CORRESPONDENCE BETWEEN PAPER AND FORMALISATIONS ###

Concepts:
1. Entities
2. Worlds
3. Existence in a world
4. Accessibility
5. B axiom or simmetry of accessibility
6. Alpha axiom
7. Beta axiom
8. Gamma axiom
9. Delta axiom
10. Conclusion
11. Negation of WL-PSR*
12. (F) 
13. (1)

Original notation in the paper:
1. (Sort E)
2. (Sort W)
3. In(a, w)
4. A(w, v)
5. ∀w∀v(A(w,v) → A(v,w))
6. ∀w∀v((∀a¬In(a,w) ∧ ∃bIn(b,v)) → ¬A(w,v))
7. ∃a∀b∀w∀v(¬In(a,v) ∨ ¬A(w,v) ∨ ¬In(b,w) ∨ In(a,w))
8. ∀a∃wIn(a,w) | `all a (exists w (In(a,w)))
9. ∀a(∃w∃v(In(a,w) ∧ ¬In(a,v)) → ∃u∃t(In(a,u) ∧ ¬In(a,t) ∧ A(u,t)))
10. ∃a∀wIn(a,w)
11. ∃a∃w∃v(In(a,w_0) ∧ ¬In(a,v) ∧ ∀b∀u(¬R(b,a) ∨ ¬In(b,u)))
12. ∀a∃b∃w∃v(¬In(a,w) ∧ In(b,w) ∧ In(a,v) ∧ A(w,v))
13. ∀a∃w∃v(¬In(a,w) ∧ In(a,v) ∧ A(w,v))

Translation into Prover9 syntax:
1. Entity(x)
2. World(x)
3. In(a, w)
4. A(w, v)
5. all w all v (World(w) & World(v) & A(w,v) -> A(v,w))
6. all w all v ((World(w) & World(v) & (all a (Entity(a) -> -In(a,w))) & (exists b (Entity(b) & In(b,v)))) -> -A(w,v))
7. exists a (Entity(a) & all b all w all v ((Entity(b) & World(w) & World(v)) -> (-In(a,v) | -A(w,v) | -In(b,w) | In(a,w))))
8. all a (Entity(a) -> exists w (World(w) & In(a,w)))
9. all a ((Entity(a) & (exists w exists v (World(w) & World(v) & In(a,w) & -In(a,v)))) -> (exists u exists t (World(u) & World(t) & In(a,u) & -In(a,t) & A(u,t))))
10. exists a (Entity(a) & all w (World(w) -> In(a,w)))
11. exists a ( Entity(a) & World(aw) & In(a, aw) & (exists v (World(v) & -In(a,v))) & all b all u ( (Entity(b) & World(u)) -> (-R(b,a) | -In(b,u)) ) ).
12. all a ( Entity(a) -> exists b exists w exists v ( Entity(b) & World(w) & World(v) & -In(a,w) & In(b,w) & In(a,v) & A(w,v) ) )
13. all a ( Entity(a) -> exists w exists v ( World(w) & World(v) & -In(a,w) & In(a,v) & A(w,v) ) )

Translation into Lean 4:
1. Entity : Type
2. World : Type
3. In : Entity → World → Prop
4. A : World → World → Prop
5. ∀ w v, frame.A w v → frame.A v w
6. ∀ w v, ( (∀ a, ¬ frame.In a w) ∧ (∃ b, frame.In b v) ) → ¬ frame.A w v
7. ∃ a, ∀ b w v, (¬ frame.In a v ∨ ¬ frame.A w v ∨ ¬ frame.In b w ∨ frame.In a w)
8. ∀ a, ∃ w, frame.In a w
9. ∀ a, ( ∃ w v, frame.In a w ∧ ¬ frame.In a v ) → ( ∃ u t, frame.In a u ∧ ¬ frame.In a t ∧ frame.A u t )
10. ∃ a, ∀ w, frame.In a w
11. (not implemented)
12. (not implemented)
13. (not implemented)

***

### CITATION ###

To use this research, please cite:

A. Montagner (2026), 'Beyond the PSR: A Necessary Entity from a Transmundane Condition of Possibility', https://doi.org/10.5281/zenodo.19629115

***

### CONTACT ###

For any inquiry, contact me at:

       Alessio Montagner
   alessio@hermesambiente.it

***

### LICENSE ###

All the proof files are released under MIT License.

***

### ACKNOWLEDGEMENTS ###

Parts of the initial formalisations were assisted by LLMs and were subsequently carefully verified and corrected.